Nuprl Definition : es-responsive 11,40

es-responsive(es;l1;tg1;l2;tg2)
== (e=rcv(l1,tg1).
== (e'=rcv(l2,tg2).
== (e loc sender(e') 
== (& (e2=rcv(l1,tg1). (e <loc e2)  (sender(e') <loc e2))
== (& (e''=rcv(l2,tg2). (sender(e'') = sender(e'))  (e'' = e')))
== & (e'=rcv(l2,tg2).
== & (e=rcv(l1,tg1).
== & (e loc sender(e') 
== & (& (e''=rcv(l2,tg2). (sender(e'') <loc sender(e'))  (sender(e'') <loc e))) 
latex



clarification:

es-responsive(es;l1;tg1;l2;tg2)
== alle-rcv(es;l1;tg1;e.existse-rcv(es;l2;tg2;e'.es-le(es;e;es-sender(es; e'))
== & alle-rcv(es;l1;tg1;e2.es-locl(es; e; e2)  es-locl(es; es-sender(es; e'); e2))
== & alle-rcv(es;l2;tg2;e''.(es-sender(es; e'') = es-sender(es; e')  es-E(es))
== &  (e'' = e'  es-E(es)))))
== & alle-rcv(es;l2;tg2;e'.existse-rcv(es;l1;tg1;e.es-le(es;e;es-sender(es; e'))
== & & alle-rcv(es;l2;tg2;e''.es-locl(es; es-sender(es; e''); es-sender(es; e'))
== & &  es-locl(es; es-sender(es; e''); e)))) 
latex


Definitionss = t, E, e=rcv(l,tg). P(e), P & Q, e loc e' , e=rcv(l,tg). P(e), P  Q, (e <loc e'), sender(e)
FDL editor aliaseses-responsive

origin